Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(apply,f_1),x)  → app(f_1,x)
2:    app(id,x)  → x
3:    app(app(app(uncurry,f_2),x),y)  → app(app(f_2,x),y)
4:    app(app(app(swap,f_2),y),x)  → app(app(f_2,x),y)
5:    app(app(app(compose,g_1),f_1),x)  → app(g_1,app(f_1,x))
6:    app(app(const,x),y)  → x
7:    app(listify,x)  → app(app(cons,x),nil)
8:    app(app(app(app(fold,f_3),g_2),x),nil)  → x
9:    app(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t))  → app(app(f_3,app(g_2,z)),app(app(app(app(fold,f_3),g_2),x),t))
10:    app(sum,l)  → app(app(app(app(fold,add),id),0),l)
11:    app(app(uncurry,app(app(fold,cons),id)),nil)  → id
12:    append  → app(app(compose,app(app(swap,fold),cons)),id)
13:    reverse  → app(app(uncurry,app(app(fold,app(swap,append)),listify)),nil)
14:    length  → app(app(uncurry,app(app(fold,add),app(cons,1))),0)
There are 32 dependency pairs:
15:    APP(app(apply,f_1),x)  → APP(f_1,x)
16:    APP(app(app(uncurry,f_2),x),y)  → APP(app(f_2,x),y)
17:    APP(app(app(uncurry,f_2),x),y)  → APP(f_2,x)
18:    APP(app(app(swap,f_2),y),x)  → APP(app(f_2,x),y)
19:    APP(app(app(swap,f_2),y),x)  → APP(f_2,x)
20:    APP(app(app(compose,g_1),f_1),x)  → APP(g_1,app(f_1,x))
21:    APP(app(app(compose,g_1),f_1),x)  → APP(f_1,x)
22:    APP(listify,x)  → APP(app(cons,x),nil)
23:    APP(listify,x)  → APP(cons,x)
24:    APP(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t))  → APP(app(f_3,app(g_2,z)),app(app(app(app(fold,f_3),g_2),x),t))
25:    APP(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t))  → APP(f_3,app(g_2,z))
26:    APP(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t))  → APP(g_2,z)
27:    APP(app(app(app(fold,f_3),g_2),x),app(app(cons,z),t))  → APP(app(app(app(fold,f_3),g_2),x),t)
28:    APP(sum,l)  → APP(app(app(app(fold,add),id),0),l)
29:    APP(sum,l)  → APP(app(app(fold,add),id),0)
30:    APP(sum,l)  → APP(app(fold,add),id)
31:    APP(sum,l)  → APP(fold,add)
32:    APPEND  → APP(app(compose,app(app(swap,fold),cons)),id)
33:    APPEND  → APP(compose,app(app(swap,fold),cons))
34:    APPEND  → APP(app(swap,fold),cons)
35:    APPEND  → APP(swap,fold)
36:    REVERSE  → APP(app(uncurry,app(app(fold,app(swap,append)),listify)),nil)
37:    REVERSE  → APP(uncurry,app(app(fold,app(swap,append)),listify))
38:    REVERSE  → APP(app(fold,app(swap,append)),listify)
39:    REVERSE  → APP(fold,app(swap,append))
40:    REVERSE  → APP(swap,append)
41:    REVERSE  → APPEND
42:    LENGTH  → APP(app(uncurry,app(app(fold,add),app(cons,1))),0)
43:    LENGTH  → APP(uncurry,app(app(fold,add),app(cons,1)))
44:    LENGTH  → APP(app(fold,add),app(cons,1))
45:    LENGTH  → APP(fold,add)
46:    LENGTH  → APP(cons,1)
The approximated dependency graph contains one SCC: {15-22,24-30}.
Tyrolean Termination Tool  (0.54 seconds)   ---  May 4, 2006